\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$a$:Knd fp$\rightarrow$ Type, ${\it init}$:$x$:Id fp$\rightarrow$ $\mathbb{Q}\rightarrow$${\it ds}$($x$)?Void,\+
\\[0ex]${\it pre}$:$a$:Id fp$\rightarrow$ State(${\it ds}$)$\rightarrow\mathbb{B}$,
\\[0ex]${\it ef}$:${\it kx}$::Knd $\times$ Id fp$\rightarrow$ State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;${\it kx}$.1)$\rightarrow\mathbb{Q}\rightarrow$${\it ds}$(${\it kx}$.2)?Void,
\\[0ex]${\it send}$:\=${\it kl}$::Knd $\times$ IdLnk fp$\rightarrow$\+
\\[0ex](${\it tg}$:Id $\times$ (State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;${\it kl}$.1)$\rightarrow$(${\it da}$(rcv(${\it kl}$.2,${\it tg}$))?Void List))) List,
\-\\[0ex]${\it frame}$:$x$:Id fp$\rightarrow$ Knd List, ${\it sframe}$:${\it ltg}$::IdLnk $\times$ Id fp$\rightarrow$ Knd List, ${\it aframe}$:$k$:Knd fp$\rightarrow$ Id List,
\\[0ex]${\it bframe}$:$k$:Knd fp$\rightarrow$ IdLnk List, ${\it rframe}$:$x$:Id fp$\rightarrow$ Knd List, ${\it prob}$:$a$:Id fp$\rightarrow$ FinProbSpace.
\-\\[0ex]ma\{\=${\it ds}$;\+
\\[0ex]${\it da}$;
\\[0ex]${\it init}$;
\\[0ex]${\it pre}$;
\\[0ex]${\it ef}$;
\\[0ex]${\it send}$;
\\[0ex]${\it frame}$;
\\[0ex]${\it sframe}$;
\\[0ex]${\it aframe}$;
\\[0ex]${\it bframe}$;
\\[0ex]${\it rframe}$;
\\[0ex]${\it prob}$\}
\-\\[0ex]$\in$ MsgA
\end{tabbing}